In this book the authors reconcile two different viewpoints of the foundations of mathematics, namely mathematical logic and category theory. In Part I, they show that typed lambda-calculi, a formulation of higher order logic, and cartesian closed categories are essentially the same. In Part II, it is demonstrated that another formulation of higher order logic is closely related to topos theory. Part III is devoted to recursive functions. Numerous applications of the close relationship between traditional logic and the algebraic language (...) of category theory are given. The authors have included an introduction to category theory and develop the necessary logic as required, making the book essentially self-contained. Detailed historical references are provided throughout, and each section concludes with a set of exercises. Thus it is well-suited for graduate courses and research in mathematics and logic. Researchers in theoretical computer science, artificial intelligence and mathematical linguistics will also find this an accessible introduction to a subject of increasing application to these disciplines. (shrink)

This book is dedicated to the life and work of the mathematician Joachim Lambek. The editors gather together noted experts to discuss the state of the art of various of Lambek’s works in logic, category theory, and linguistics and to celebrate his contributions to those areas over the course of his multifaceted career. After early work in combinatorics and elementary number theory, Lambek became a distinguished algebraist. In the 1960s, he began to work in category theory, categorical algebra, logic, proof (...) theory, and foundations of computability. In a parallel development, beginning in the late 1950s and for the rest of his career, Lambek also worked extensively in mathematical linguistics and computational approaches to natural languages. He and his collaborators perfected production and type grammars for numerous natural languages. Lambek grammars form an early noncommutative precursor to Girard’s linear logic. In a surprising development, he introduced a novel and deeper algebraic framework for analyzing natural language, along with algebraic, higher category, and proof-theoretic semantics. This book is of interest to mathematicians, logicians, linguists, and computer scientists. (shrink)